\begin{tabbing}
es{-}sends{-}iff2(${\it es}$;$l$;${\it tg}$;$B$;${\it ds}$;$e$.$P$($e$);$e$.$f$($e$))
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(($\forall$$e$:E. (kind($e$) = rcv($l$,${\it tg}$)) $\Rightarrow$ (valtype($e$) $\subseteq$r $B$))\+
\\[0ex]\& ($\forall$$x$:Id. vartype(source($l$);$x$) $\subseteq$r ${\it ds}$($x$)?Top))
\\[0ex]c$\wedge$ \=($\forall$$e$@source($l$). $P$($e$) $\Rightarrow$ ($\exists$${\it e'}$:E. ((kind(${\it e'}$) = rcv($l$,${\it tg}$)) c$\wedge$ (sender(${\it e'}$) = $e$)))\+
\\[0ex]\& ($\forall$${\it e'}$:E. (kind(${\it e'}$) = rcv($l$,${\it tg}$)) $\Rightarrow$ ($P$(sender(${\it e'}$)) c$\wedge$ (val(${\it e'}$) = $f$(sender(${\it e'}$)))))
\\[0ex]\& (\=$\forall$${\it e'}$:E.\+
\\[0ex](kind(${\it e'}$) = rcv($l$,${\it tg}$))
\\[0ex]$\Rightarrow$ \=($\forall$${\it e''}$:E.\+
\\[0ex]($\uparrow$isrcv(${\it e''}$))
\\[0ex]$\Rightarrow$ (lnk(${\it e''}$) = $l$)
\\[0ex]$\Rightarrow$ (sender(${\it e''}$) = sender(${\it e'}$))
\\[0ex]$\Rightarrow$ (${\it e''}$ = ${\it e'}$))))
\-\-\-\-
\end{tabbing}